| Definitions | t  T, SESAxioms{i:l}(E; T; pred?; info; when; after),  x:A. B(x),  x:A. B(x), Top, x:A B(x), EventsWithValues, AtomFreeDecls(X), P   Q, 2of(t), <a,b>, 1of(t), A & B, P & Q, EOrderAxioms(E; pred?; info),  b, destination(l), rcv(l,tg), f(a), locl(a), kindcase(k; a.f(a); l,t.g(l;t) ), Type, AtomFree(T;x), Knd, Id, lnk(k), tag(k), act(k), islocal(k), left+right, ESAtomAxiom{i:l}(T;V), x:A  B(x), S  T, e < e', Void, False,  A, first(e), {x:A| B(x) }, pred(e), s = t, SWellFounded(R(x;y)), IdLnk,  x:A. B(x), P  Q, S  T, Unit, EqDecider(T), kind(e), isrcv(k), sender(e), loc(e), IdLnkDeq, sends(dE;dL;pred?;info;val;p;e;l), Msg(M), ||as||, a<b, #$n, A B, i j < k, index(dE;dL;pred?;info;p;r),  , True,  T, {i..j }, Prop, pred!(e;e'), link(e), receives(dE;dL;pred?;info;p;e;l), rcv-from-on(dE;dL;info;e;l;r), Msg_sub(l;M), type List, eventtype(k;loc;V;M;e), mk-es0(E;eq;T;V;M;loc;k;v;w;a;snds;sndr;i;f;prd;cl;p;q),  x.A(x), ecase1(e;info;i.f(i);l,e'.g(l;e')), rcv?(e),  , dstype(TypeNames; d; a), SqStable(P), s ~ t,  x,y. t(x;y), x. t(x) |